; <lemma>
;  <title>ssf.3</title>
;  <origin>ssf | rec2 | cbuf_read/inv6/INV</origin>
; <lemma>
;  <title>ssf.1</title>
;  <origin>ssf | rec2 | cbuf_write/inv6/INV</origin>
(benchmark ssf_3
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="n" type="INTEGER"/>
;    <variable name="x" type="INTEGER"/>
;    <variable name="y" type="INTEGER"/>
;  </typenv>
  :extrafuns ((n Int)
	       (x Int)
	       (y Int))
  :extramacros (
		 (in (lambda (?x 't) (?p ('t boolean)) . (?p ?x)))
		 (Nat (lambda (?i Int) . (<= 0 ?i)))

		 (subseteq
		   (lambda (?p ('t boolean)) (?q ('t boolean)) .
		     (forall (?x 't). 
		       (implies (?p ?x) (?q ?x)))))
		 (subset
		   (lambda (?p ('t boolean)) (?q ('t boolean)) .
		     (and (subseteq ?p ?q)
		       (not (= ?p ?q)))))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 )
; <hypothesis needed="true">n : NATURAL</hypothesis>
  :assumption (in n Nat)
; <hypothesis needed="true">x : NATURAL</hypothesis>
  :assumption (in x Nat)
; <hypothesis needed="true">y : NATURAL</hypothesis>
  :assumption (in y Nat)
; <hypothesis needed="true">x - y : 0 .. n</hypothesis>
  :assumption (in (- x y) (range 0 n))
; <hypothesis needed="true">y &lt; x</hypothesis>
  :assumption (< y x)
; <goal>x - (y+1) : 0 .. n</goal>
  :formula
  (not
    (in
      (- x (+ y 1))
      (range 0 n))
    )
)
; </lemma>
